b:. (b = ff)  ((b)) 

latex

ProofTree

Definitions	, t  T, P  Q, P  Q, P  Q, P  Q, x:A. B(x), if b then t else f fi , b, ff, True, tt, b, Unit, , False, A,
Lemmas	bnot wf, assert wf, bfalse wf, bool wf, btrue neq bfalse, assert of ff